-
Notifications
You must be signed in to change notification settings - Fork 316
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(Analysis/Normed/Group/Ultra): triangle ineq for tsum & tprod #17584
base: master
Are you sure you want to change the base?
Conversation
loefflerd
commented
Oct 9, 2024
PR summary bc3cc9747f
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Analysis.Normed.Group.Ultra | 1178 | 1186 | +8 (+0.68%) |
Import changes for all files
Files | Import difference |
---|---|
Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Ring.Ultra |
8 |
Declarations diff
+ nnnorm_tprod_le
+ nnnorm_tprod_le_of_forall_le
+ norm_tprod_le
+ norm_tprod_le_of_forall_le
+ norm_tprod_le_of_forall_le_of_nonneg
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh
contains some details about this script.
Do you think it would be appropriate here to add similar lemmas for
`finprod` and `finsum`? You could use the `⨆ (i : s)` syntax to avoid the
set-conditionally-complete-lattice problem. Lemmas like `tprod_eq_finprod`
could help golf using the lemmas proven here.
…On Wed, Oct 9, 2024 at 10:18 AM github-actions[bot] < ***@***.***> wrote:
PR summary ebfb2f9
<ebfb2f9> Import
changes for modified files
Dependency changes
File Base Count Head Count Change
Mathlib.Analysis.Normed.Group.Ultra 1178 1186 +8 (+0.68%) Import changes
for all files
Files Import difference
Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Ring.Ultra 8
------------------------------
Declarations diff
+ nnnorm_tprod_le
+ norm_tprod_le
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh contains some details
about this script.
—
Reply to this email directly, view it on GitHub
<#17584 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABIYHBS2KYO6WLGJWH3CSOTZ2U3LFAVCNFSM6AAAAABPUU5R4CVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMBSGQ4DAMBXGQ>
.
You are receiving this because your review was requested.Message ID:
***@***.***>
|
I thought you might say that 😄 The issue is that we would have multiple formulations to choose from (Finset.sup, Finset.sup', iSup over a subtype, sSup of the range), and I'm not sure which is best. I'd rather not add more API for the finite case in this particular PR; but if you think it's valuable, by all means make a separate PR for it. In a somewhat opposite direction, I was actually thinking that it might be a good idea to have the tsum/tprod versions of (As for golfing using |
Fair! I thought since we |